es:ES, i, x:Id, T:Type, v:T.
@i x initially v:T  @i only [] affect x:T  e@i. (x when e) = v 

latex

Definitions	Knd, A, True, if b then t else f fi , tt, P  Q, P  Q, P & Q, b, e@i. P(e), A c B, x. t(x), t  T, , @i always.P(x), P  Q, x:A. B(x), False, {T}, SQType(T), @i(x:T), @i only L affect x:T, @i x initially v:T, x(s)
Lemmas	IdLnk wf, nil member, false wf, es-kind wf, l member wf, not functionality wrt iff, es-after wf, es-E wf, es-first wf, assert wf, es-init-identity, Id sq, es-first-init, es-when-first-discrete, es-loc wf, es-when wf, es-vartype wf, es-initially wf, es-dtype wf, es-loc-init, event system wf, Id wf, init-p wf, Knd wf, es-frame wf, es-invariant1